Reasoning about Polymorphic Functions
A polymorphic function is a function that is generic over a type parameter, behaving the same for every type.
For example, consider the function reverse[A] :List A -> List A, which inverts the order of a list. The elements
of the list can be of an arbitrary type A. We can show the following property of reverse:
reverse (map f xs) = map f (reverse xs), for any list xs and function f. In words: applying a function f to
every element of a list and then reverting is yields the same result as reverting the list and then applying f to
every element. Surprisingly, this can be proven without knowing the definition of reverse, but just by looking at its type!
The idea is that reverse has to behave the same way for every type A, so it can't make decisions based on the specific values of the elements;
it can only shuffle, duplicate, and remove elements.
This principle of parametricity allows deriving these so-called free theorems for all kinds of polymorphic types. The original approach for semi-automatically deriving these theorems from types has been given by Wadler Wadler, but since then, simpler approaches have been proposed (see References).
In the seminar, you will look at and compare approaches to deriving free theorems from parametric types. You will also use a free theorem generator to derive free theorems for example types.